T:Type{i}, L:T List, R:({x:T| (x  L) }es_realizer{i:l}), P:({x:T| (x  L) }ES{i}Prop{i'}).
(x, y:T. Dec(x = y))
 (xL. R(x) ||-{i} es.P(x,es))
 (xL. yL. x = y  T  R-compat{i:l}(R(x); R(y)))
 xL.R(x) ||-{i} es.xL. P(x,es) 

latex

Definitions	x. t(x), t  T, x(s1,s2), x(s), xL. P(x), P  Q, Prop, x:A. B(x), {T}, P  Q, Dec(P)
Lemmas	es realizer wf, decidable wf, event system wf, R-realizes wf, R-compat wf, not wf, l member wf, R-all-rule